package org.eclipse.iota.rules;

import java.util.HashSet;
import java.util.List;
import java.util.Set;

import org.eclipse.iota.assignments.Assignment;
import org.eclipse.iota.assignments.SubstitutionAssignmentGenerator;
import org.eclipse.iota.model.Clause;
import org.eclipse.iota.model.Constraint;
import org.eclipse.iota.model.Equation;
import org.eclipse.iota.model.Inclusion;
import org.eclipse.iota.model.Parameter;
import org.eclipse.iota.model.Property;
import org.eclipse.iota.model.Reference;
import org.eclipse.iota.model.Variable;
import org.eclipse.iota.rewrite.AbstractIotaRule;
import org.eclipse.iota.util.IotaFindUtil;
import org.eclipse.iota.util.IotaVariableUtil;

/**
 * @author Christian Krause
 * @generated NOT
 */
public class FindRecursion extends AbstractIotaRule {
	
	@Override
	public boolean apply(Clause clause, boolean change) {
		
		// Check if it can be applied.
		if (!canApplyToClause(clause)) return false;
		
		// Create a substitutions generator.
		SubstitutionAssignmentGenerator generator = new SubstitutionAssignmentGenerator();
		
		// We are not looking for identity assignments.
		generator.setAllowIdentity(false);
		
		// Source variables: only the predicate parameters.
		generator.getSources().addAll(clause.getAlternation().getDefinition().getParameters());
		
		// Target variables: all variables.
		generator.getTargets().addAll(IotaVariableUtil.getVariables(clause));
		
		// Source and target constraints.
		for (Constraint constraint : clause.getConstraints()) {
			if (!constraint.isInferred()) {
				generator.getSourceConstraints().add(constraint);
			}
			generator.getTargetConstraints().add(constraint);
		}
		
		// Compute the assignments.
		List<Assignment> assigments = generator.calculateAssigments();
		
		if (!assigments.isEmpty()) {

			Set<Constraint> deleting = new HashSet<Constraint>();			
			for (Assignment assignment : assigments) {
				
				// Create an inclusion object.
				Inclusion inclusion = createInclusion(assignment, clause);
				
				// Remove the matched target constraints.
				for (Constraint source : generator.getSourceConstraints()) {
					Constraint target = generator.findTargetConstraint(source, assignment);
					if (target.isInferred()) deleting.add(target);
				}
				
				// Add the inclusion.
				if (change && !IotaFindUtil.contains(clause, inclusion)) {
					clause.getConstraints().add(inclusion);
				}
			}
			if (change) {
				clause.getConstraints().removeAll(deleting);
			}
			return true;
		}
		
		return false;

	}
	
	/*
	 * Check if infinite descent can be apllied to the given clause.
	 */
	private boolean canApplyToClause(Clause clause) {
		// There should be at least one equation which involves one of the parameters.
		for (Constraint constraint : clause.getConstraints()) {
			if (constraint instanceof Equation) {
				Equation equation = (Equation) constraint;
				for (Variable variable : IotaVariableUtil.getUsedVariables(equation)) {
					if (clause.getAlternation().getDefinition().getParameters().contains(variable)) return true;
				}
			}
		}
		return false;
	}

	/*
	 * Create an inclusion object based on an assignment.
	 */
	private Inclusion createInclusion(Assignment assignment, Clause clause) {
		Inclusion inclusion = new Inclusion((Property) clause.getAlternation().getDefinition());	// This can fail!!!
		for (Parameter parameter : clause.getAlternation().getDefinition().getParameters()) {
			inclusion.getArguments().add(((Reference) assignment.get(parameter)).getVariable() );
		}
		return inclusion;
	}
}
